\begin{tabbing}
$\forall$\=${\it es}$:ES, $P$:(E$\rightarrow\mathbb{P}$), $p$:($\forall$$e$:E. Dec($P$($e$))), $Q$, $R$:(E$\rightarrow$E$\rightarrow\mathbb{P}$), $A$, $B$:Type, ${\it Ia}$:AbsInterface($A$),\+
\\[0ex]${\it Ib}$:AbsInterface($B$), $f$:(E(${\it Ia}$)$\rightarrow$$B$), $g$:(E(${\it Ib}$)$\rightarrow$E), $q$:($\forall$$e$:E. Dec(($\uparrow$($e$ $\in_{b}$ ${\it Ib}$)) c$\wedge$ $P$($g$($e$)))).
\-\\[0ex]($\forall$$e$:E. ($\uparrow$($e$ $\in_{b}$ ${\it Ib}$)) $\Rightarrow$ $P$($g$($e$)))
\\[0ex]$\Rightarrow$ $g$ glues (${\it Ia}$$\mid$$p$):$Q$ $--$$f$$\rightarrow$ (${\it Ib}$$\mid$$q$):$R$
\\[0ex]$\Rightarrow$ $g$ glues (${\it Ia}$$\mid$$p$):$Q$ $--$$f$$\rightarrow$ ${\it Ib}$:$R$
\end{tabbing}